<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Issue4580NegativeLiterals</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Comment">-- Andreas, 2020-04-12, issue #4580</a>
<a id="37" class="Comment">-- Highlighting for builtins FROMNAT, FROMNEG, FROMSTRING</a>

<a id="96" class="Keyword">open</a> <a id="101" class="Keyword">import</a> <a id="108" href="Agda.Builtin.Nat.html" class="Module">Agda.Builtin.Nat</a>
<a id="125" class="Keyword">open</a> <a id="130" class="Keyword">import</a> <a id="137" href="Agda.Builtin.Equality.html" class="Module">Agda.Builtin.Equality</a>

<a id="160" class="Keyword">record</a> <a id="Number"></a><a id="167" href="Issue4580NegativeLiterals.html#167" class="Record">Number</a> <a id="174" class="Symbol">(</a><a id="175" href="Issue4580NegativeLiterals.html#175" class="Bound">A</a> <a id="177" class="Symbol">:</a> <a id="179" href="Agda.Primitive.html#388" class="Primitive">Set</a><a id="182" class="Symbol">)</a> <a id="184" class="Symbol">:</a> <a id="186" href="Agda.Primitive.html#388" class="Primitive">Set</a> <a id="190" class="Keyword">where</a>
  <a id="198" class="Keyword">field</a> <a id="Number.fromNat"></a><a id="204" href="Issue4580NegativeLiterals.html#204" class="Field">fromNat</a> <a id="212" class="Symbol">:</a> <a id="214" href="Agda.Builtin.Nat.html#203" class="Datatype">Nat</a> <a id="218" class="Symbol">→</a> <a id="220" href="Issue4580NegativeLiterals.html#175" class="Bound">A</a>

<a id="223" class="Keyword">record</a> <a id="Negative"></a><a id="230" href="Issue4580NegativeLiterals.html#230" class="Record">Negative</a> <a id="239" class="Symbol">(</a><a id="240" href="Issue4580NegativeLiterals.html#240" class="Bound">A</a> <a id="242" class="Symbol">:</a> <a id="244" href="Agda.Primitive.html#388" class="Primitive">Set</a><a id="247" class="Symbol">)</a> <a id="249" class="Symbol">:</a> <a id="251" href="Agda.Primitive.html#388" class="Primitive">Set</a> <a id="255" class="Keyword">where</a>
  <a id="263" class="Keyword">field</a> <a id="Negative.fromNeg"></a><a id="269" href="Issue4580NegativeLiterals.html#269" class="Field">fromNeg</a> <a id="277" class="Symbol">:</a> <a id="279" href="Agda.Builtin.Nat.html#203" class="Datatype">Nat</a> <a id="283" class="Symbol">→</a> <a id="285" href="Issue4580NegativeLiterals.html#240" class="Bound">A</a>

<a id="288" class="Keyword">open</a> <a id="293" href="Issue4580NegativeLiterals.html#167" class="Module">Number</a> <a id="300" class="Symbol">{{...}}</a> <a id="308" class="Keyword">public</a>
<a id="315" class="Keyword">open</a> <a id="320" href="Issue4580NegativeLiterals.html#230" class="Module">Negative</a> <a id="329" class="Symbol">{{...}}</a> <a id="337" class="Keyword">public</a>

<a id="345" class="Symbol">{-#</a> <a id="349" class="Keyword">BUILTIN</a> <a id="357" class="Keyword">FROMNAT</a> <a id="365" href="Issue4580NegativeLiterals.html#204" class="Field">fromNat</a> <a id="373" class="Symbol">#-}</a>  <a id="378" class="Comment">-- Should be highlighted.</a>
<a id="404" class="Symbol">{-#</a> <a id="408" class="Keyword">BUILTIN</a> <a id="416" class="Keyword">FROMNEG</a> <a id="424" href="Issue4580NegativeLiterals.html#269" class="Field">fromNeg</a> <a id="432" class="Symbol">#-}</a>  <a id="437" class="Comment">-- Jump to definition should work.</a>

<a id="473" class="Keyword">instance</a>
  <a id="NumberNat"></a><a id="484" href="Issue4580NegativeLiterals.html#484" class="Function">NumberNat</a> <a id="494" class="Symbol">:</a> <a id="496" href="Issue4580NegativeLiterals.html#167" class="Record">Number</a> <a id="503" href="Agda.Builtin.Nat.html#203" class="Datatype">Nat</a>
  <a id="509" href="Issue4580NegativeLiterals.html#484" class="Function">NumberNat</a> <a id="519" class="Symbol">=</a> <a id="521" class="Keyword">record</a> <a id="528" class="Symbol">{</a> <a id="530" href="Issue4580NegativeLiterals.html#204" class="Field">fromNat</a> <a id="538" class="Symbol">=</a> <a id="540" class="Symbol">λ</a> <a id="542" href="Issue4580NegativeLiterals.html#542" class="Bound">n</a> <a id="544" class="Symbol">→</a> <a id="546" href="Issue4580NegativeLiterals.html#542" class="Bound">n</a> <a id="548" class="Symbol">}</a>

<a id="551" class="Keyword">data</a> <a id="Int"></a><a id="556" href="Issue4580NegativeLiterals.html#556" class="Datatype">Int</a> <a id="560" class="Symbol">:</a> <a id="562" href="Agda.Primitive.html#388" class="Primitive">Set</a> <a id="566" class="Keyword">where</a>
  <a id="Int.pos"></a><a id="574" href="Issue4580NegativeLiterals.html#574" class="InductiveConstructor">pos</a> <a id="578" class="Symbol">:</a> <a id="580" href="Agda.Builtin.Nat.html#203" class="Datatype">Nat</a> <a id="584" class="Symbol">→</a> <a id="586" href="Issue4580NegativeLiterals.html#556" class="Datatype">Int</a>
  <a id="Int.neg"></a><a id="592" href="Issue4580NegativeLiterals.html#592" class="InductiveConstructor">neg</a> <a id="596" class="Symbol">:</a> <a id="598" href="Agda.Builtin.Nat.html#203" class="Datatype">Nat</a> <a id="602" class="Symbol">→</a> <a id="604" href="Issue4580NegativeLiterals.html#556" class="Datatype">Int</a>

<a id="609" class="Keyword">instance</a>
  <a id="NumberInt"></a><a id="620" href="Issue4580NegativeLiterals.html#620" class="Function">NumberInt</a> <a id="630" class="Symbol">:</a> <a id="632" href="Issue4580NegativeLiterals.html#167" class="Record">Number</a> <a id="639" href="Issue4580NegativeLiterals.html#556" class="Datatype">Int</a>
  <a id="645" href="Issue4580NegativeLiterals.html#620" class="Function">NumberInt</a> <a id="655" class="Symbol">=</a> <a id="657" class="Keyword">record</a> <a id="664" class="Symbol">{</a> <a id="666" href="Issue4580NegativeLiterals.html#204" class="Field">fromNat</a> <a id="674" class="Symbol">=</a> <a id="676" href="Issue4580NegativeLiterals.html#574" class="InductiveConstructor">pos</a> <a id="680" class="Symbol">}</a>

  <a id="NegativeInt"></a><a id="685" href="Issue4580NegativeLiterals.html#685" class="Function">NegativeInt</a> <a id="697" class="Symbol">:</a> <a id="699" href="Issue4580NegativeLiterals.html#230" class="Record">Negative</a> <a id="708" href="Issue4580NegativeLiterals.html#556" class="Datatype">Int</a>
  <a id="714" href="Issue4580NegativeLiterals.html#685" class="Function">NegativeInt</a> <a id="726" class="Symbol">=</a> <a id="728" class="Keyword">record</a> <a id="735" class="Symbol">{</a> <a id="737" href="Issue4580NegativeLiterals.html#269" class="Field">fromNeg</a> <a id="745" class="Symbol">=</a> <a id="747" class="Symbol">λ</a> <a id="749" class="Symbol">{</a> <a id="751" href="Agda.Builtin.Nat.html#221" class="InductiveConstructor">zero</a> <a id="756" class="Symbol">→</a> <a id="758" href="Issue4580NegativeLiterals.html#574" class="InductiveConstructor">pos</a> <a id="762" class="Number">0</a> <a id="764" class="Symbol">;</a> <a id="766" class="Symbol">(</a><a id="767" href="Agda.Builtin.Nat.html#234" class="InductiveConstructor">suc</a> <a id="771" href="Issue4580NegativeLiterals.html#771" class="Bound">n</a><a id="772" class="Symbol">)</a> <a id="774" class="Symbol">→</a> <a id="776" href="Issue4580NegativeLiterals.html#592" class="InductiveConstructor">neg</a> <a id="780" href="Issue4580NegativeLiterals.html#771" class="Bound">n</a> <a id="782" class="Symbol">}</a> <a id="784" class="Symbol">}</a>

<a id="minusFive"></a><a id="787" href="Issue4580NegativeLiterals.html#787" class="Function">minusFive</a> <a id="797" class="Symbol">:</a> <a id="799" href="Issue4580NegativeLiterals.html#556" class="Datatype">Int</a>
<a id="803" href="Issue4580NegativeLiterals.html#787" class="Function">minusFive</a> <a id="813" class="Symbol">=</a> <a id="815" class="Number">-5</a>

<a id="thm"></a><a id="819" href="Issue4580NegativeLiterals.html#819" class="Function">thm</a> <a id="823" class="Symbol">:</a> <a id="825" class="Number">-5</a> <a id="828" href="Agda.Builtin.Equality.html#150" class="Datatype Operator">≡</a> <a id="830" href="Issue4580NegativeLiterals.html#592" class="InductiveConstructor">neg</a> <a id="834" class="Number">4</a>
<a id="836" href="Issue4580NegativeLiterals.html#819" class="Function">thm</a> <a id="840" class="Symbol">=</a> <a id="842" href="Agda.Builtin.Equality.html#207" class="InductiveConstructor">refl</a>
</pre></body></html>